module fn.logic.fol.syntax.Scheme

open System.Collections.Generic

open fn.adt.Tree
open fn.adt.tree.Transform
open fn.adt.tree.search.Pattern

open fn.logic.fol.syntax.Formula



type FolTemplate = FolFormula<Wild<Identifier,Identifier>>

type FolScheme (template : FolTemplate, placeholders : Identifier list) =
    member this.template = template
    member this.placeholders = placeholders
    
    member this.pattern
        with get() = TreeTopPattern(this.template.e)
    
    new (template : FolScheme, placeholders) = FolScheme(template.template, placeholders)

    new (template : FolTemplate) =
        FolScheme(template, [for n in template.e.nodes do
                             match n with
                             | Any x -> yield x
                             | _ -> ()])
    
    override this.GetHashCode() = (this.template, this.placeholders).GetHashCode()
    override this.Equals (other : obj) = 
        match other with
        | :? FolScheme as x -> (this.template, this.placeholders).Equals((x.template, x.placeholders))
        | _ -> false
    
    override this.ToString() = this.template.ToString()

    static member atom (r : Wild<Identifier,Identifier>) = FolScheme(FolTemplate.atom r)
    static member atom (r : Identifier) = FolScheme(FolTemplate.atom (Literal r))
    
    member this.instantiate (fillin : IDictionary<_,_>) =
        let modif (Tree.Node(r, _) as tree) =
            match r with
            | Wild.Literal x -> Root x
            | Wild.Any m -> Subtree fillin.[m]
        let e' = MappingTreeTransform(modif) =~ this.template.e
        FolFormula(e')
    
    member this.instantiate_partial (fillin : IDictionary<_,_>) =
        let to_wild_lit (x : Tree<_>) = Root (Wild.Literal x.root)
        let to_scheme_lit = MappingTreeTransform(to_wild_lit).apply
        let modif (Tree.Node(r, _) as tree) =
            match r with
            | Wild.Any m when fillin.ContainsKey(m) -> Subtree (to_scheme_lit fillin.[m])
            | _ -> Nop
        let e' = MappingTreeTransform(modif) =~ this.template.e
        FolScheme(FolTemplate(e'))
    
    static member (=~) (scheme : FolScheme, phi : FolFormula) = scheme.pattern =~ phi.e
    


let (|SchemeTemplate|_|) (scheme : FolScheme) =
    Some scheme.template

let (|Scheme|_|) (scheme : FolScheme) (formula : FolFormula) =
    let mo = scheme =~ formula
    match mo with
    | Some d -> Some [for v in scheme.placeholders -> FolFormula d.[v]]
    | None -> None

